Hi @strub, the PR is almost ready; I specifically prepared it in a "TDD" way.

An upside of the proposed patch is that it is not necessary to exclude Coq versions before 8.12.1.

However the job build (mathcomp/mathcomp:1.12.0-coq-8.12) still fails in a weird way:
https://github.com/math-comp/multinomials/pull/45/checks?check_run_id=3727362037

@ejgallego do you have a idea of what's missing?

do you have a idea of what's missing?

On second thought I guess this is precisely what we had documented in this section:

https://github.com/coq/ceps/blob/master/text/048-packaging-coq-native.md#note-to-library-developers-and-package-maintainers

Roughly, in order to ensure that coq-mathcomp-ssreflect are native-compiled with Coq < 8.13, one should just apply the CEP 48 / item 3 strategy (given coq-mathcomp-ssreflect is built using coq_makefile) in the coq-opam-archive…

I'll try do to this soon.

Cc @proux01 @CohenCyril FYI

We can also just forget about Coq < 8.13 and coq-native, it would already be great to have things working with Coq >= 8.13. I'm not sure there are much users of Coq < 8.13 and native_compute around. native_compute with anything using multinomials is broken for more than six months now, having it work even with Coq >= 8.13 would be a huge progress.

I really don't care. My point is rather: don't put too much effort in supporting older versions as there isn't much use for it. Of course, if it's easy why not. But I'd really prefer something working with current versions to something not working at all.

I really don't care. My point is rather: don't put too much effort in supporting older versions as there isn't much use for it. Of course, if it's easy why not. But I'd really prefer something working with current versions to something not working at all.

Same for me.

I really don't care. My point is rather: don't put too much effort in supporting older versions as there isn't much use for it. Of course, if it's easy why not. But I'd really prefer something working with current versions to something not working at all.

OK. Regarding the effort involved, I'd say the vast majority of this effort is already done! (discussing and refining the CEP, preparing and merging the coq-native package, proposing a workflow to adapt packaging for both dune and coq_makefile).

Anyway, I agree with your pragmatism:

• Even if we could apply item 3 to all packages in a systematic way, it should be enough to apply it to a minimal set of dependencies (roughly, mathcomp.1.12.0) that is required for users to also benefit from native_compute in their (CoqEAL, Coq-8.12) based project;
• So FYI I opened this PR: feat: Take advantage of the coq-native package (CEP 048, item 3) coq/opam#1835;
• But to avoid delaying the merge of this PR, I guess I will push a tiny extra commit that won't require having (coq.8.12, mathcomp.1.12.0, coq-native) working… but that we'll be able to trivially revert later on after the merge of coq/opam-coq-archive#1835.

I will push a tiny extra commit that won't require having (coq.8.12, mathcomp.1.12.0, coq-native) working…

done. Does this look good to you?

LGTM However, this looks quite heavy, we'll definitely need to fix dune when 3.0 will be there to avoid such painful work.

@erikmd indeed that error usually happens when the native files for a depending library weren't compiled.